nLab Daniel Licata

• website

Selected writings

On programming in homotopy type theory:

• Programming in Homotopy Type Theory, Talk at IFIP Wroking Group 2.8 meeting, November, 2012 (pdf, pdf)

Introduction to basics of synthetic homotopy theory in terms of homotopy type theory:

• Guillaume Brunerie, Dan Licata, Peter LeFanu Lumsdaine: Homotopy theory in type theory, 2013 (pdf slides, pdf, blog entry 1, blog entry 2)

Formalization of (the proof of) the Blakers-Massey theorem in homotopy type theory:

• Kuen-Bang Hou (Favonia), Eric Finster, Dan Licata, Peter LeFanu Lumsdaine, A mechanization of the Blakers-Massey connectivity theorem in Homotopy Type Theory, LICS ‘16 (2016) 565–574 [arXiv.1605.03227, doi:10.1145/2933575.2934545]

On adjoint logic:

• Daniel Licata, Mike Shulman, and Mitchell Riley, A Fibrational Framework for Substructural and Modal Logics (extended version), in Proceedings of 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017) (doi: 10.4230/LIPIcs.FSCD.2017.25, pdf)

On synthetic (∞,1)-category theory in cubical type theory with bicubical sets:

• Matthew Weaver, Daniel Licata, A Constructive Model of Directed Univalence in Bicubical Sets, in: Proceedings of the 35th Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’20, Association for Computing Machinery (2020) 915–928 [doi:10.1145/3373718.3394794]

On homotopy dependent linear type theory of dependent stable homotopy types with categorical semantics in parametrized spectra:

• Mitchell Riley, Eric Finster, Daniel Licata, Synthetic Spectra via a Monadic and Comonadic Modality (arXiv:2102.04099)

category: people